#if 0
// Definitions for using x86 performance monitoring counters
#ifndef PIOS_KERN_PMC_H_
#define PIOS_KERN_PMC_H_

#include <types.h>
#include <determinator.h>

#if det==1
	extern bool pmc_avail;	// true if PMC instruction counting is available
	extern int pmc_safety;	// safety margin required to account for overshoot
	extern int pmc_overshoot; // max overshoot we've observed so far
	extern void (*pmc_set)(int maxcnt);
	extern int (*pmc_get)(int maxcnt);

	void pmc_init(void);
#endif

#endif /* PIOS_KERN_PMC_H_ */
#endif
